<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Equiv: Program Equivalence</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://www.cis.upenn.edu/~bcpierce/sf/current/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 2: Programming Language Foundations</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>Table of Contents</li></a>
   <a href='coqindex.html'><li class='section_name'>Index</li></a>
   <a href='deps.html'><li class='section_name'>Roadmap</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Equiv<span class="subtitle">Program Equivalence</span></h1>


<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Maps</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Bool.Bool</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.Arith</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Init.Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.PeanoNat</span>. <span class="id" type="keyword">Import</span> <span class="id" type="var">Nat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Arith.EqNat</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">omega.Omega</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Lists.List</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">Coq</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Logic.FunctionalExtensionality</span>.<br/>
<span class="id" type="keyword">Import</span> <span class="id" type="var">ListNotations</span>.<br/>
<span class="id" type="var">From</span> <span class="id" type="var">PLF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Import</span> <span class="id" type="var">Imp</span>.<br/>
</div>

<div class="doc">
<a name="lab8"></a><h3 class="section">Some Advice for Working on Exercises:</h3>


<div class="paragraph"> </div>

<ul class="doclist">
<li> Most of the Coq proofs we ask you to do are similar to proofs
      that we've provided.  Before starting to work on exercises
      problems, take the time to work through our proofs (both
      informally and in Coq) and make sure you understand them in
      detail.  This will save you a lot of time.

<div class="paragraph"> </div>


</li>
<li> The Coq proofs we're doing now are sufficiently complicated that
      it is more or less impossible to complete them by random
      experimentation or "following your nose."  You need to start
      with an idea about why the property is true and how the proof is
      going to go.  The best way to do this is to write out at least a
      sketch of an informal proof on paper &mdash; one that intuitively
      convinces you of the truth of the theorem &mdash; before starting to
      work on the formal one.  Alternately, grab a friend and try to
      convince them that the theorem is true; then try to formalize
      your explanation.

<div class="paragraph"> </div>


</li>
<li> Use automation to save work!  The proofs in this chapter can get
      pretty long if you try to write out all the cases explicitly. 
</li>
</ul>

</div>

<div class="doc">
<a name="lab9"></a><h1 class="section">Behavioral Equivalence</h1>

<div class="paragraph"> </div>

 In an earlier chapter, we investigated the correctness of a very
    simple program transformation: the <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> function.  The
    programming language we were considering was the first version of
    the language of arithmetic expressions &mdash; with no variables &mdash; so
    in that setting it was very easy to define what it means for a
    program transformation to be correct: it should always yield a
    program that evaluates to the same number as the original.

<div class="paragraph"> </div>

    To talk about the correctness of program transformations for the
    full Imp language, in particular assignment, we need to consider
    the role of variables and state. 
</div>

<div class="doc">
<a name="lab10"></a><h2 class="section">Definitions</h2>

<div class="paragraph"> </div>

 For <span class="inlinecode"><span class="id" type="var">aexp</span></span>s and <span class="inlinecode"><span class="id" type="var">bexp</span></span>s with variables, the definition we want is
    clear: Two <span class="inlinecode"><span class="id" type="var">aexp</span></span>s or <span class="inlinecode"><span class="id" type="var">bexp</span></span>s are <i>behaviorally equivalent</i> if
    they evaluate to the same result in every state. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">aequiv</span> (<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">bequiv</span> (<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>1</sub></span> = <span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b<sub>2</sub></span>.<br/>
</div>

<div class="doc">
Here are some simple examples of equivalences of arithmetic
    and boolean expressions. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">aequiv_example</span>: <span class="id" type="var">aequiv</span> (<span class="id" type="var">X</span> - <span class="id" type="var">X</span>) 0.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">bequiv_example</span>: <span class="id" type="var">bequiv</span> (<span class="id" type="var">X</span> - <span class="id" type="var">X</span> = 0)%<span class="id" type="var">imp</span> <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">beval</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">aequiv_example</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
For commands, the situation is a little more subtle.  We can't
    simply say "two commands are behaviorally equivalent if they
    evaluate to the same ending state whenever they are started in the
    same initial state," because some commands, when run in some
    starting states, don't terminate in any final state at all!  What
    we need instead is this: two commands are behaviorally equivalent
    if, for any given starting state, they either (1) both diverge
    or (2) both terminate in the same final state.  A compact way to
    express this is "if the first one terminates in a particular state
    then so does the second, and vice versa." 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>) ↔ (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>).<br/>
</div>

<div class="doc">
<a name="lab11"></a><h2 class="section">Simple Examples</h2>

<div class="paragraph"> </div>

 For examples of command equivalence, let's start by looking at
    some trivial program transformations involving <span class="inlinecode"><span class="id" type="var">SKIP</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_left</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">SKIP</span>;; <span class="id" type="var">c</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab12"></a><h4 class="section">Exercise: 2 stars, standard (skip_right)</h4>
 Prove that adding a <span class="inlinecode"><span class="id" type="var">SKIP</span></span> after a command results in an
    equivalent program 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">skip_right</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">c</span> ;; <span class="id" type="var">SKIP</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Similarly, here is a simple transformation that optimizes <span class="inlinecode"><span class="id" type="var">TEST</span></span>
    commands: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_true_simple</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">true</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Of course, no (human) programmer would write a conditional whose
    guard is literally <span class="inlinecode"><span class="id" type="var">true</span></span>.  But they might write one whose guard
    is <i>equivalent</i> to true:  <i>Theorem</i>: If <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, then <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>. 
<div class="paragraph"> </div>

   <i>Proof</i>:

<div class="paragraph"> </div>

<ul class="doclist">
<li> (<span class="inlinecode">→</span>) We must show, for all <span class="inlinecode"><span class="id" type="var">st</span></span> and <span class="inlinecode"><span class="id" type="var">st'</span></span>, that if <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span>
       <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> then <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.

<div class="paragraph"> </div>

       Proceed by cases on the rules that could possibly have been
       used to show <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>, namely
       <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> and <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose the final rule in the derivation of <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span>
         <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> was <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span>.  We then have,
         by the premises of <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span>, that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.
         This is exactly what we set out to prove.

<div class="paragraph"> </div>


</li>
<li> On the other hand, suppose the final rule in the derivation
         of <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> was <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>.
         We then know that <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> and <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.

<div class="paragraph"> </div>

         Recall that <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, i.e., forall <span class="inlinecode"><span class="id" type="var">st</span></span>,
         <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span>.  In particular, this means
         that <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>, since <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>.  But
         this is a contradiction, since <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span> requires that
         <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>.  Thus, the final rule could not have
         been <span class="inlinecode"><span class="id" type="var">E_IfFalse</span></span>.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> (<span class="inlinecode">&lt;-</span>) We must show, for all <span class="inlinecode"><span class="id" type="var">st</span></span> and <span class="inlinecode"><span class="id" type="var">st'</span></span>, that if
       <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> then
       <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.

<div class="paragraph"> </div>

       Since <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, we know that <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> =
       <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> = <span class="inlinecode"><span class="id" type="var">true</span></span>.  Together with the assumption that
       <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>, we can apply <span class="inlinecode"><span class="id" type="var">E_IfTrue</span></span> to derive
       <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">TEST</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">THEN</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">ELSE</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode"><span class="id" type="var">FI</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.  <span class="proofbox">&#9744;</span>

</li>
</ul>

<div class="paragraph"> </div>

   Here is the formal version of this proof: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_true</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;evaluates&nbsp;to&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;evaluates&nbsp;to&nbsp;false&nbsp;(contradiction)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">simpl</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab13"></a><h4 class="section">Exercise: 2 stars, standard, recommended (TEST_false)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">TEST_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab14"></a><h4 class="section">Exercise: 3 stars, standard (swap_if_branches)</h4>
 Show that we can swap the branches of an IF if we also negate its
    guard. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">swap_if_branches</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">BNot</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 For <span class="inlinecode"><span class="id" type="var">WHILE</span></span> loops, we can give a similar pair of theorems.  A loop
    whose guard is equivalent to <span class="inlinecode"><span class="id" type="var">BFalse</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">SKIP</span></span>,
    while a loop whose guard is equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span> is equivalent to
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">BTrue</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">SKIP</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> (or any other non-terminating program).
    The first of these facts is easy. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_false</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BFalse</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">Hb</span>. <span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab15"></a><h4 class="section">Exercise: 2 stars, advanced, optional (WHILE_false_informal)</h4>
 Write an informal proof of <span class="inlinecode"><span class="id" type="var">WHILE_false</span></span>.

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

 To prove the second fact, we need an auxiliary lemma stating that
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> loops whose guards are equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span> never
    terminate. 
<div class="paragraph"> </div>

 <i>Lemma</i>: If <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">BTrue</span></span>, then it cannot be
    the case that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: Suppose that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.  We show,
    by induction on a derivation of <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>,
    that this assumption leads to a contradiction. The only two cases
    to consider are <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> and <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>, the others
    are contradictory.

<div class="paragraph"> </div>

<ul class="doclist">
<li> Suppose <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> is proved using rule
      <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span>.  Then by assumption <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span>.  But
      this contradicts the assumption that <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to
      <span class="inlinecode"><span class="id" type="var">BTrue</span></span>.

<div class="paragraph"> </div>


</li>
<li> Suppose <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> is proved using rule
      <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>.  We must have that:

<div class="paragraph"> </div>

      1. <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>,
      2. there is some <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> such that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> and
         <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>,
      3. and we are given the induction hypothesis that
         <span class="inlinecode"><span class="id" type="var">st<sub>0</sub></span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> leads to a contradiction,

<div class="paragraph"> </div>

      We obtain a contradiction by 2 and 3. <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">WHILE_true_nonterm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">BTrue</span> →<br/>
&nbsp;&nbsp;~( <span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st'</span> ).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">cw</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqcw</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H</span>;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Most&nbsp;rules&nbsp;don't&nbsp;apply;&nbsp;we&nbsp;rule&nbsp;them&nbsp;out&nbsp;by&nbsp;inversion:&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqcw</span>; <span class="id" type="tactic">subst</span>; <span class="id" type="tactic">clear</span> <span class="id" type="var">Heqcw</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;two&nbsp;interesting&nbsp;cases&nbsp;are&nbsp;the&nbsp;ones&nbsp;for&nbsp;WHILE&nbsp;loops:&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span> <span class="comment">(*&nbsp;contradictory&nbsp;--&nbsp;b&nbsp;is&nbsp;always&nbsp;true!&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>&nbsp;is&nbsp;able&nbsp;to&nbsp;instantiate&nbsp;the&nbsp;quantifier&nbsp;in&nbsp;<span class="inlinecode"><span class="id" type="var">st</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hb</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span> <span class="comment">(*&nbsp;immediate&nbsp;from&nbsp;the&nbsp;IH&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHceval2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab16"></a><h4 class="section">Exercise: 2 stars, standard, optional (WHILE_true_nonterm_informal)</h4>
 Explain what the lemma <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span> means in English.

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab17"></a><h4 class="section">Exercise: 2 stars, standard, recommended (WHILE_true)</h4>
 Prove the following theorem. <i>Hint</i>: You'll want to use
    <span class="inlinecode"><span class="id" type="var">WHILE_true_nonterm</span></span> here. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">WHILE_true</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">true</span>  →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 A more interesting fact about <span class="inlinecode"><span class="id" type="var">WHILE</span></span> commands is that any number
    of copies of the body can be "unrolled" without changing meaning.
    Loop unrolling is a common transformation in real compilers. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">loop_unrolling</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> (<span class="id" type="var">c</span> ;; <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span>) <span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hce</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;loop&nbsp;doesn't&nbsp;run&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfFalse</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;loop&nbsp;runs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_IfTrue</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>). <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;loop&nbsp;runs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'0</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;loop&nbsp;doesn't&nbsp;run&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>5</sub></span>; <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">assumption</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab18"></a><h4 class="section">Exercise: 2 stars, standard, optional (seq_assoc)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">seq_assoc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> ((<span class="id" type="var">c<sub>1</sub></span>;;<span class="id" type="var">c<sub>2</sub></span>);;<span class="id" type="var">c<sub>3</sub></span>) (<span class="id" type="var">c<sub>1</sub></span>;;(<span class="id" type="var">c<sub>2</sub></span>;;<span class="id" type="var">c<sub>3</sub></span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Proving program properties involving assignments is one place
    where the fact that program states are treated
    extensionally (e.g., <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode"><span class="id" type="var">m</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">m</span></span> and <span class="inlinecode"><span class="id" type="var">m</span></span> are equal maps) comes
    in handy. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">identity_assignment</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intro</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">t_update_same</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Skip</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hx</span> : <span class="id" type="var">st'</span> =[ <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">x</span> ]⇒ (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">st'</span> <span class="id" type="var">x</span> ; <span class="id" type="var">st'</span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>. <span class="id" type="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">t_update_same</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hx</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hx</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab19"></a><h4 class="section">Exercise: 2 stars, standard, recommended (assign_aequiv)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">assign_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) <span class="id" type="var">e</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">x</span> <span class="id" type="var">e</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">SKIP</span> (<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">e</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab20"></a><h4 class="section">Exercise: 2 stars, standard (equiv_classes)</h4>

<div class="paragraph"> </div>

 Given the following programs, group together those that are
    equivalent in Imp. Your answer should be given as a list of lists,
    where each sub-list represents a group of equivalent programs. For
    example, if you think programs (a) through (h) are all equivalent
    to each other, but not to (i), your answer should look like this:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[&nbsp;[<span class="id" type="var">prog_a</span>;<span class="id" type="var">prog_b</span>;<span class="id" type="var">prog_c</span>;<span class="id" type="var">prog_d</span>;<span class="id" type="var">prog_e</span>;<span class="id" type="var">prog_f</span>;<span class="id" type="var">prog_g</span>;<span class="id" type="var">prog_h</span>]&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[<span class="id" type="var">prog_i</span>]&nbsp;]
<div class="paragraph"> </div>

</div>
    Write down your answer below in the definition of
    <span class="inlinecode"><span class="id" type="var">equiv_classes</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_a</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> ≤ 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_b</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0 <span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1<br/>
&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;<span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - <span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_c</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">SKIP</span>%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_d</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> (<span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_e</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_f</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_g</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_h</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">X</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">prog_i</span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">Y</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">equiv_classes</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">com</span>)<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_equiv_classes</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab21"></a><h1 class="section">Properties of Behavioral Equivalence</h1>

<div class="paragraph"> </div>

 We next consider some fundamental properties of program
    equivalence. 
</div>

<div class="doc">
<a name="lab22"></a><h2 class="section">Behavioral Equivalence Is an Equivalence</h2>

<div class="paragraph"> </div>

 First, we verify that the equivalences on <span class="inlinecode"><span class="id" type="var">aexps</span></span>, <span class="inlinecode"><span class="id" type="var">bexps</span></span>, and
    <span class="inlinecode"><span class="id" type="var">com</span></span>s really are <i>equivalences</i> &mdash; i.e., that they are reflexive,
    symmetric, and transitive.  The proofs are all easy. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>), <span class="id" type="var">aequiv</span> <span class="id" type="var">a</span> <span class="id" type="var">a</span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_aequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> → <span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">a<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>), <span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">b</span>.<br/>
<div class="togglescript" id="proofcontrol10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')"><span class="show"></span></div>
<div class="proofscript" id="proof10" onclick="toggleDisplay('proof10');toggleDisplay('proofcontrol10')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')"><span class="show"></span></div>
<div class="proofscript" id="proof11" onclick="toggleDisplay('proof11');toggleDisplay('proofcontrol11')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>. <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_bequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> → <span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')"><span class="show"></span></div>
<div class="proofscript" id="proof12" onclick="toggleDisplay('proof12');toggleDisplay('proofcontrol12')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span> <span class="id" type="var">b<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">rewrite</span> (<span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span>). <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">refl_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c</span> : <span class="id" type="var">com</span>), <span class="id" type="var">cequiv</span> <span class="id" type="var">c</span> <span class="id" type="var">c</span>.<br/>
<div class="togglescript" id="proofcontrol13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')"><span class="show"></span></div>
<div class="proofscript" id="proof13" onclick="toggleDisplay('proof13');toggleDisplay('proofcontrol13')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">iff_refl</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">sym_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>1</sub></span>.<br/>
<div class="togglescript" id="proofcontrol14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')"><span class="show"></span></div>
<div class="proofscript" id="proof14" onclick="toggleDisplay('proof14');toggleDisplay('proofcontrol14')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">H</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> ↔ <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">H'</span>.<br/>
&nbsp;&nbsp;{ <span class="comment">(*&nbsp;Proof&nbsp;of&nbsp;assertion&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_sym</span>. <span class="id" type="tactic">assumption</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">iff_trans</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P<sub>1</sub></span> <span class="id" type="var">P<sub>2</sub></span> <span class="id" type="var">P<sub>3</sub></span> : <span class="id" type="keyword">Prop</span>),<br/>
&nbsp;&nbsp;(<span class="id" type="var">P<sub>1</sub></span> ↔ <span class="id" type="var">P<sub>2</sub></span>) → (<span class="id" type="var">P<sub>2</sub></span> ↔ <span class="id" type="var">P<sub>3</sub></span>) → (<span class="id" type="var">P<sub>1</sub></span> ↔ <span class="id" type="var">P<sub>3</sub></span>).<br/>
<div class="togglescript" id="proofcontrol15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')"><span class="show"></span></div>
<div class="proofscript" id="proof15" onclick="toggleDisplay('proof15');toggleDisplay('proofcontrol15')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P<sub>1</sub></span> <span class="id" type="var">P<sub>2</sub></span> <span class="id" type="var">P<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>12</sub></span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>23</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">A</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">A</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">trans_cequiv</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>3</sub></span>.<br/>
<div class="togglescript" id="proofcontrol16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')"><span class="show"></span></div>
<div class="proofscript" id="proof16" onclick="toggleDisplay('proof16');toggleDisplay('proofcontrol16')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">cequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">H<sub>12</sub></span> <span class="id" type="var">H<sub>23</sub></span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">iff_trans</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>12</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>23</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab23"></a><h2 class="section">Behavioral Equivalence Is a Congruence</h2>

<div class="paragraph"> </div>

 Less obviously, behavioral equivalence is also a <i>congruence</i>.
    That is, the equivalence of two subprograms implies the
    equivalence of the larger programs in which they are embedded:
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">aequiv&nbsp;a<sub>1</sub>&nbsp;a<sub>1</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;(x&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;a<sub>1</sub>)&nbsp;(x&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;a<sub>1</sub>')</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;c<sub>1</sub>&nbsp;c<sub>1</sub>'</td>
  <td></td>
</td>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;c<sub>2</sub>&nbsp;c<sub>2</sub>'</td>
  <td class="infrulenamecol" rowspan="3">
    &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">cequiv&nbsp;(c<sub>1</sub>;;c<sub>2</sub>)&nbsp;(c<sub>1</sub>';;c<sub>2</sub>')</td>
  <td></td>
</td>
</table></center>    ... and so on for the other forms of commands. 
<div class="paragraph"> </div>

 (Note that we are using the inference rule notation here not
    as part of a definition, but simply to write down some valid
    implications in a readable format. We prove these implications
    below.) 
<div class="paragraph"> </div>

 We will see a concrete example of why these congruence
    properties are important in the following section (in the proof of
    <span class="inlinecode"><span class="id" type="var">fold_constants_com_sound</span></span>), but the main idea is that they allow
    us to replace a small part of a large program with an equivalent
    small part and know that the whole large programs are equivalent
    <i>without</i> doing an explicit proof about the non-varying parts &mdash;
    i.e., the "proof burden" of a small change to a large program is
    proportional to the size of the change, not the program. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CAss_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">CAss</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub>'</span>).<br/>
<div class="togglescript" id="proofcontrol17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')"><span class="show"></span></div>
<div class="proofscript" id="proof17" onclick="toggleDisplay('proof17');toggleDisplay('proofcontrol17')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> <span class="id" type="var">Heqv</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hceval</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">Hceval</span>. <span class="id" type="tactic">subst</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heqv</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
The congruence property for loops is a little more interesting,
    since it requires induction.

<div class="paragraph"> </div>

    <i>Theorem</i>: Equivalence is a congruence for <span class="inlinecode"><span class="id" type="var">WHILE</span></span> &mdash; that is, if
    <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span>, then
    <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: Suppose <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> is
    equivalent to <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span>.  We must show, for every <span class="inlinecode"><span class="id" type="var">st</span></span> and <span class="inlinecode"><span class="id" type="var">st'</span></span>, that
    <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> iff <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span>
    <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.  We consider the two directions separately.

<div class="paragraph"> </div>

<ul class="doclist">
<li> (<span class="inlinecode">→</span>) We show that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> implies
        <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>, by induction on a
        derivation of <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.  The only
        nontrivial cases are when the final rule in the derivation is
        <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> or <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span>: In this case, the form of the rule gives us
            <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">false</span></span> and <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>.  But then, since
            <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> are equivalent, we have <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode">=</span>
            <span class="inlinecode"><span class="id" type="var">false</span></span>, and <span class="inlinecode"><span class="id" type="var">E_WhileFalse</span></span> applies, giving us
            <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>, as required.

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span>: The form of the rule now gives us <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span>
            <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>, with <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span> and <span class="inlinecode"><span class="id" type="var">st'0</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span>
            <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span> for some state <span class="inlinecode"><span class="id" type="var">st'0</span></span>, with the
            induction hypothesis <span class="inlinecode"><span class="id" type="var">st'0</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span>
            <span class="inlinecode"><span class="id" type="var">st'</span></span>.

<div class="paragraph"> </div>

            Since <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> are equivalent, we know that <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span>
            <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'0</span></span>.  And since <span class="inlinecode"><span class="id" type="var">b<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> are equivalent,
            we have <span class="inlinecode"><span class="id" type="var">beval</span></span> <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>.  Now <span class="inlinecode"><span class="id" type="var">E_WhileTrue</span></span> applies,
            giving us <span class="inlinecode"><span class="id" type="var">st</span></span> <span class="inlinecode">=[</span> <span class="inlinecode"><span class="id" type="var">WHILE</span></span> <span class="inlinecode"><span class="id" type="var">b<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">DO</span></span> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub>'</span></span> <span class="inlinecode"><span class="id" type="var">END</span></span> <span class="inlinecode">]⇒</span> <span class="inlinecode"><span class="id" type="var">st'</span></span>, as
            required.

<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> (<span class="inlinecode">&lt;-</span>) Similar. <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CWhile_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">END</span>) (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">END</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>,<span class="id" type="var">cequiv</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">Hb1e</span> <span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>; <span class="id" type="tactic">intros</span> <span class="id" type="var">Hce</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">cwhile</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">eqn</span>:<span class="id" type="var">Heqcwhile</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqcwhile</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;show&nbsp;loop&nbsp;runs&nbsp;*)</span> <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;body&nbsp;execution&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">Hce1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;subsequent&nbsp;loop&nbsp;execution&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHce2</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">DO</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">END</span>)%<span class="id" type="var">imp</span> <span class="id" type="keyword">as</span> <span class="id" type="var">c'while</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">eqn</span>:<span class="id" type="var">Heqc'while</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hce</span>; <span class="id" type="tactic">inversion</span> <span class="id" type="var">Heqc'while</span>; <span class="id" type="tactic">subst</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileFalse&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileFalse</span>. <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;E_WhileTrue&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_WhileTrue</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := <span class="id" type="var">st'</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;show&nbsp;loop&nbsp;runs&nbsp;*)</span> <span class="id" type="tactic">rewrite</span> → <span class="id" type="var">Hb1e</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;body&nbsp;execution&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">Hc1e</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>). <span class="id" type="tactic">apply</span> <span class="id" type="var">Hce1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="comment">(*&nbsp;subsequent&nbsp;loop&nbsp;execution&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">IHHce2</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab24"></a><h4 class="section">Exercise: 3 stars, standard, optional (CSeq_congruence)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CSeq_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span>;;<span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="var">c<sub>1</sub>'</span>;;<span class="id" type="var">c<sub>2</sub>'</span>).<br/>
<div class="togglescript" id="proofcontrol18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')"><span class="show"></span></div>
<div class="proofscript" id="proof18" onclick="toggleDisplay('proof18');toggleDisplay('proofcontrol18')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<br/>
</div>

<div class="doc">
<a name="lab25"></a><h4 class="section">Exercise: 3 stars, standard (CIf_congruence)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">CIf_congruence</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">b'</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> <span class="id" type="var">b'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>1</sub>'</span> → <span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">c<sub>2</sub>'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">TEST</span> <span class="id" type="var">b'</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub>'</span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub>'</span> <span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 For example, here are two equivalent programs and a proof of their
    equivalence... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">congruence_example</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Program&nbsp;1:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 42<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">FI</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Program&nbsp;2:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> <span class="id" type="var">X</span> = 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">THEN</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - <span class="id" type="var">X</span>   <span class="comment">(*&nbsp;&lt;---&nbsp;Changed&nbsp;here&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 42<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">FI</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">CSeq_congruence</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">CIf_congruence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_bequiv</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">CAss_congruence</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">symmetry</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">minus_diag</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab26"></a><h4 class="section">Exercise: 3 stars, advanced, optional (not_congr)</h4>
 We've shown that the <span class="inlinecode"><span class="id" type="var">cequiv</span></span> relation is both an equivalence and
    a congruence on commands.  Can you think of a relation on commands
    that is an equivalence but <i>not</i> a congruence? 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab27"></a><h1 class="section">Program Transformations</h1>

<div class="paragraph"> </div>

 A <i>program transformation</i> is a function that takes a program as
    input and produces some variant of the program as output.
    Compiler optimizations such as constant folding are a canonical
    example, but there are many others. 
<div class="paragraph"> </div>

 A program transformation is <i>sound</i> if it preserves the
    behavior of the original program. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">atrans_sound</span> (<span class="id" type="var">atrans</span> : <span class="id" type="var">aexp</span> → <span class="id" type="var">aexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aequiv</span> <span class="id" type="var">a</span> (<span class="id" type="var">atrans</span> <span class="id" type="var">a</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">btrans_sound</span> (<span class="id" type="var">btrans</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">bexp</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> (<span class="id" type="var">btrans</span> <span class="id" type="var">b</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">ctrans_sound</span> (<span class="id" type="var">ctrans</span> : <span class="id" type="var">com</span> → <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">c</span> : <span class="id" type="var">com</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">c</span> (<span class="id" type="var">ctrans</span> <span class="id" type="var">c</span>).<br/>
</div>

<div class="doc">
<a name="lab28"></a><h2 class="section">The Constant-Folding Transformation</h2>

<div class="paragraph"> </div>

 An expression is <i>constant</i> when it contains no variable
    references.

<div class="paragraph"> </div>

    Constant folding is an optimization that finds constant
    expressions and replaces them by their values. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_aexp</span> (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span>       ⇒ <span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> <span class="id" type="var">x</span>        ⇒ <span class="id" type="var">AId</span> <span class="id" type="var">x</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> - <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒ <span class="id" type="var">ANum</span> (<span class="id" type="var">n<sub>1</sub></span> * <span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒ <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_aexp_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> ((1 + 2) * <span class="id" type="var">X</span>) <br/>
&nbsp;&nbsp;= (3 * <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')"><span class="show"></span></div>
<div class="proofscript" id="proof19" onclick="toggleDisplay('proof19');toggleDisplay('proofcontrol19')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Note that this version of constant folding doesn't eliminate
    trivial additions, etc. &mdash; we are focusing attention on a single
    optimization for the sake of simplicity.  It is not hard to
    incorporate other ways of simplifying expressions; the definitions
    and proofs just get longer. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_aexp_ex<sub>2</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> (<span class="id" type="var">X</span> - ((0 * 6) + <span class="id" type="var">Y</span>))%<span class="id" type="var">imp</span> = (<span class="id" type="var">X</span> - (0 + <span class="id" type="var">Y</span>))%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')"><span class="show"></span></div>
<div class="proofscript" id="proof20" onclick="toggleDisplay('proof20');toggleDisplay('proofcontrol20')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
Not only can we lift <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> to <span class="inlinecode"><span class="id" type="var">bexp</span></span>s (in the
    <span class="inlinecode"><span class="id" type="var">BEq</span></span> and <span class="inlinecode"><span class="id" type="var">BLe</span></span> cases); we can also look for constant <i>boolean</i>
    expressions and evaluate them in-place. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_bexp</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bexp</span>) : <span class="id" type="var">bexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>        ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BFalse</span>       ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n<sub>1</sub></span> =? <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">BEq</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>1</sub></span>, <span class="id" type="var">ANum</span> <span class="id" type="var">n<sub>2</sub></span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">n<sub>1</sub></span> &lt;=? <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="keyword">then</span> <span class="id" type="var">BTrue</span> <span class="id" type="keyword">else</span> <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">a<sub>1</sub>'</span>, <span class="id" type="var">a<sub>2</sub>'</span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">BLe</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">a<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span> ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b<sub>1</sub>'</span> ⇒ <span class="id" type="var">BNot</span> <span class="id" type="var">b<sub>1</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub></span> <span class="id" type="var">b<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>, <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>2</sub></span>) <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BTrue</span>) ⇒ <span class="id" type="var">BTrue</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BTrue</span>, <span class="id" type="var">BFalse</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BTrue</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">BFalse</span>, <span class="id" type="var">BFalse</span>) ⇒ <span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| (<span class="id" type="var">b<sub>1</sub>'</span>, <span class="id" type="var">b<sub>2</sub>'</span>) ⇒ <span class="id" type="var">BAnd</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">b<sub>2</sub>'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_bexp_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> (<span class="id" type="var">true</span> &amp;&amp; ~(<span class="id" type="var">false</span> &amp;&amp; <span class="id" type="var">true</span>))%<span class="id" type="var">imp</span> <br/>
&nbsp;&nbsp;= <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')"><span class="show"></span></div>
<div class="proofscript" id="proof21" onclick="toggleDisplay('proof21');toggleDisplay('proofcontrol21')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_bexp_ex<sub>2</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span> ((<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) &amp;&amp; (0 = (2 - (1 + 1))))%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= ((<span class="id" type="var">X</span> = <span class="id" type="var">Y</span>) &amp;&amp; <span class="id" type="var">true</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')"><span class="show"></span></div>
<div class="proofscript" id="proof22" onclick="toggleDisplay('proof22');toggleDisplay('proofcontrol22')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
To fold constants in a command, we apply the appropriate folding
    functions on all embedded expressions. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp</span>.<br/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold_constants_com</span> (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>) : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">c</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">SKIP</span>      ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a</span>   ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span>) ;; (<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span>  ⇒ <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b'</span> ⇒ <span class="id" type="var">TEST</span> <span class="id" type="var">b'</span> <span class="id" type="var">THEN</span> <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BTrue</span> ⇒ <span class="id" type="var">WHILE</span> <span class="id" type="var">BTrue</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">BFalse</span> ⇒ <span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">b'</span> ⇒ <span class="id" type="var">WHILE</span> <span class="id" type="var">b'</span> <span class="id" type="var">DO</span> (<span class="id" type="var">fold_constants_com</span> <span class="id" type="var">c</span>) <span class="id" type="var">END</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_com_ex<sub>1</sub></span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_constants_com</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Original&nbsp;program:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 4 + 5;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - 3;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) = (2 + 4) <span class="id" type="var">THEN</span> <span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0 <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> 0 ≤ (4 - (2 + 1)) <span class="id" type="var">THEN</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span> <span class="id" type="var">Y</span> = 0 <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= <span class="comment">(*&nbsp;After&nbsp;constant&nbsp;folding:&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 9;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> - 3;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">TEST</span> (<span class="id" type="var">X</span> - <span class="id" type="var">Y</span>) = 6 <span class="id" type="var">THEN</span> <span class="id" type="var">SKIP</span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ELSE</span> <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0 <span class="id" type="var">FI</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span> <span class="id" type="var">Y</span> = 0 <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')"><span class="show"></span></div>
<div class="proofscript" id="proof23" onclick="toggleDisplay('proof23');toggleDisplay('proofcontrol23')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab29"></a><h2 class="section">Soundness of Constant Folding</h2>

<div class="paragraph"> </div>

 Now we need to show that what we've done is correct. 
<div class="paragraph"> </div>

 Here's the proof for arithmetic expressions: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_aexp_sound</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">atrans_sound</span> <span class="id" type="var">fold_constants_aexp</span>.<br/>
<div class="togglescript" id="proofcontrol24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')"><span class="show"></span></div>
<div class="proofscript" id="proof24" onclick="toggleDisplay('proof24');toggleDisplay('proofcontrol24')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">atrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">a</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">aequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">a</span>; <span class="id" type="tactic">simpl</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;ANum&nbsp;and&nbsp;AId&nbsp;follow&nbsp;immediately&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;APlus,&nbsp;AMinus,&nbsp;and&nbsp;AMult&nbsp;follow&nbsp;from&nbsp;the&nbsp;IH<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;and&nbsp;the&nbsp;observation&nbsp;that<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;aeval&nbsp;st&nbsp;(APlus&nbsp;a<sub>1</sub>&nbsp;a<sub>2</sub>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;ANum&nbsp;((aeval&nbsp;st&nbsp;a<sub>1</sub>)&nbsp;+&nbsp;(aeval&nbsp;st&nbsp;a<sub>2</sub>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;aeval&nbsp;st&nbsp;(ANum&nbsp;((aeval&nbsp;st&nbsp;a<sub>1</sub>)&nbsp;+&nbsp;(aeval&nbsp;st&nbsp;a<sub>2</sub>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(and&nbsp;similarly&nbsp;for&nbsp;AMinus/minus&nbsp;and&nbsp;AMult/mult)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa1</span>; <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHa2</span>; <span class="id" type="tactic">reflexivity</span>). <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab30"></a><h4 class="section">Exercise: 3 stars, standard, optional (fold_bexp_Eq_informal)</h4>
 Here is an informal proof of the <span class="inlinecode"><span class="id" type="var">BEq</span></span> case of the soundness
    argument for boolean expression constant folding.  Read it
    carefully and compare it to the formal proof that follows.  Then
    fill in the <span class="inlinecode"><span class="id" type="var">BLe</span></span> case of the formal proof (without looking at the
    <span class="inlinecode"><span class="id" type="var">BEq</span></span> case, if possible).

<div class="paragraph"> </div>

   <i>Theorem</i>: The constant folding function for booleans,
   <span class="inlinecode"><span class="id" type="var">fold_constants_bexp</span></span>, is sound.

<div class="paragraph"> </div>

   <i>Proof</i>: We must show that <span class="inlinecode"><span class="id" type="var">b</span></span> is equivalent to <span class="inlinecode"><span class="id" type="var">fold_constants_bexp</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span>,
   for all boolean expressions <span class="inlinecode"><span class="id" type="var">b</span></span>.  Proceed by induction on <span class="inlinecode"><span class="id" type="var">b</span></span>.  We
   show just the case where <span class="inlinecode"><span class="id" type="var">b</span></span> has the form <span class="inlinecode"><span class="id" type="var">BEq</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>.

<div class="paragraph"> </div>

   In this case, we must show

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_bexp</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)).
<div class="paragraph"> </div>

</div>
   There are two cases to consider:

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, suppose <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> and
       <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ANum</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> for some <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span>.

<div class="paragraph"> </div>

       In this case, we have

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold_constants_bexp</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>
<div class="paragraph"> </div>

</div>
       and

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
       By the soundness of constant folding for arithmetic
       expressions (Lemma <span class="inlinecode"><span class="id" type="var">fold_constants_aexp_sound</span></span>), we know

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>
<div class="paragraph"> </div>

</div>
       and

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>2</sub></span>,
<div class="paragraph"> </div>

</div>
       so

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.
<div class="paragraph"> </div>

</div>
       Also, it is easy to see (by considering the cases <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> and
       <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span></span> separately) that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">BFalse</span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">true</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">false</span><br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.
<div class="paragraph"> </div>

</div>
       So

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>.<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n<sub>1</sub></span>&nbsp;=?&nbsp;<span class="id" type="var">n<sub>2</sub></span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">BTrue</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">BFalse</span>),
<div class="paragraph"> </div>

</div>
       as required.

<div class="paragraph"> </div>


</li>
<li> Otherwise, one of <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> and
       <span class="inlinecode"><span class="id" type="var">fold_constants_aexp</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span> is not a constant.  In this case, we
       must show

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;<span class="id" type="var">beval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">BEq</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)),
<div class="paragraph"> </div>

</div>
       which, by the definition of <span class="inlinecode"><span class="id" type="var">beval</span></span>, is the same as showing

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)&nbsp;=?&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;=&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>))&nbsp;=?<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)).
<div class="paragraph"> </div>

</div>
       But the soundness of constant folding for arithmetic
       expressions (<span class="inlinecode"><span class="id" type="var">fold_constants_aexp_sound</span></span>) gives us

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>&nbsp;=&nbsp;<span class="id" type="var">aeval</span>&nbsp;<span class="id" type="var">st</span>&nbsp;(<span class="id" type="var">fold_constants_aexp</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>),
<div class="paragraph"> </div>

</div>
       completing the case.  <span class="proofbox">&#9744;</span> 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_bexp_sound</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">btrans_sound</span> <span class="id" type="var">fold_constants_bexp</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">btrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">b</span>. <span class="id" type="tactic">unfold</span> <span class="id" type="var">bequiv</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">st</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">b</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;BTrue&nbsp;and&nbsp;BFalse&nbsp;are&nbsp;immediate&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BEq&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
(Doing induction when there are a lot of constructors makes
    specifying variable names a chore, but Coq doesn't always
    choose nice variable names.  We can rename entries in the
    context with the <span class="inlinecode"><span class="id" type="tactic">rename</span></span> tactic: <span class="inlinecode"><span class="id" type="tactic">rename</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode"><span class="id" type="var">into</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> will
    change <span class="inlinecode"><span class="id" type="var">a</span></span> to <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> in the current goal and context.) 
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>1</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a<sub>1</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqa1'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_aexp</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">a<sub>2</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqa2'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">replace</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub>'</span>) <span class="id" type="tactic">by</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">subst</span> <span class="id" type="var">a<sub>1</sub>'</span>; <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">fold_constants_aexp_sound</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">replace</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub></span>) <span class="id" type="keyword">with</span> (<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>2</sub>'</span>) <span class="id" type="tactic">by</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">subst</span> <span class="id" type="var">a<sub>2</sub>'</span>; <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">fold_constants_aexp_sound</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>1</sub>'</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">a<sub>2</sub>'</span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">reflexivity</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;only&nbsp;interesting&nbsp;case&nbsp;is&nbsp;when&nbsp;both&nbsp;a<sub>1</sub>&nbsp;and&nbsp;a<sub>2</sub><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;become&nbsp;constants&nbsp;after&nbsp;folding&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? <span class="id" type="var">n<sub>0</sub></span>); <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BLe&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">admit</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BNot&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">b'</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;BAnd&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>1</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b<sub>1</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb1'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b<sub>2</sub></span>) <span class="id" type="keyword">as</span> <span class="id" type="var">b<sub>2</sub>'</span> <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb2'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb1</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHb2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">b<sub>1</sub>'</span>; <span class="id" type="tactic">destruct</span> <span class="id" type="var">b<sub>2</sub>'</span>; <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab31"></a><h4 class="section">Exercise: 3 stars, standard (fold_constants_com_sound)</h4>
 Complete the <span class="inlinecode"><span class="id" type="var">WHILE</span></span> case of the following proof. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_constants_com_sound</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">ctrans_sound</span> <span class="id" type="var">fold_constants_com</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">ctrans_sound</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">c</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">c</span>; <span class="id" type="tactic">simpl</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;SKIP&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">refl_cequiv</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">CAss_congruence</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">fold_constants_aexp_sound</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;;;&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">CSeq_congruence</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;TEST&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">bequiv</span> <span class="id" type="var">b</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>)). {<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">fold_constants_bexp_sound</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> (<span class="id" type="var">fold_constants_bexp</span> <span class="id" type="var">b</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">Heqb</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">apply</span> <span class="id" type="var">CIf_congruence</span>; <span class="id" type="tactic">assumption</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;(If&nbsp;the&nbsp;optimization&nbsp;doesn't&nbsp;eliminate&nbsp;the&nbsp;if,&nbsp;then&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;result&nbsp;is&nbsp;easy&nbsp;to&nbsp;prove&nbsp;from&nbsp;the&nbsp;IH&nbsp;and<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" type="var">fold_constants_bexp_sound</span></span>.)&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;always&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">trans_cequiv</span> <span class="id" type="keyword">with</span> <span class="id" type="var">c<sub>1</sub></span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">TEST_true</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;b&nbsp;always&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">trans_cequiv</span> <span class="id" type="keyword">with</span> <span class="id" type="var">c<sub>2</sub></span>; <span class="id" type="tactic">try</span> <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">TEST_false</span>; <span class="id" type="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;WHILE&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab32"></a><h3 class="section">Soundness of (0 + n) Elimination, Redux</h3>

<div class="paragraph"> </div>

<a name="lab33"></a><h4 class="section">Exercise: 4 stars, advanced, optional (optimize_0plus)</h4>
 Recall the definition <span class="inlinecode"><span class="id" type="var">optimize_0plus</span></span> from the <a href="https://www.cis.upenn.edu/~bcpierce/sf/lf-current/Imp.html"><span class="inlineref">Imp</span></a> chapter of <i>Logical
    Foundations</i>:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span>&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;(<span class="id" type="var">e</span>:<span class="id" type="var">aexp</span>)&nbsp;:&nbsp;<span class="id" type="var">aexp</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span>&nbsp;<span class="id" type="var">e</span>&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ANum</span>&nbsp;<span class="id" type="var">n</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">APlus</span>&nbsp;(<span class="id" type="var">ANum</span>&nbsp;0)&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">APlus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">APlus</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">AMinus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMinus</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">AMult</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>&nbsp;⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMult</span>&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>1</sub></span>)&nbsp;(<span class="id" type="var">optimize_0plus</span>&nbsp;<span class="id" type="var">e<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.
<div class="paragraph"> </div>

</div>
   Note that this function is defined over the old <span class="inlinecode"><span class="id" type="var">aexp</span></span>s,
   without states.

<div class="paragraph"> </div>

   Write a new version of this function that accounts for variables,
   plus analogous ones for <span class="inlinecode"><span class="id" type="var">bexp</span></span>s and commands:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_aexp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_bexp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">optimize_0plus_com</span>
<div class="paragraph"> </div>

</div>
   Prove that these three functions are sound, as we did for
   <span class="inlinecode"><span class="id" type="var">fold_constants_</span>*</span>.  Make sure you use the congruence lemmas in
   the proof of <span class="inlinecode"><span class="id" type="var">optimize_0plus_com</span></span> &mdash; otherwise it will be <i>long</i>!

<div class="paragraph"> </div>

   Then define an optimizer on commands that first folds
   constants (using <span class="inlinecode"><span class="id" type="var">fold_constants_com</span></span>) and then eliminates <span class="inlinecode">0</span> <span class="inlinecode">+</span> <span class="inlinecode"><span class="id" type="var">n</span></span>
   terms (using <span class="inlinecode"><span class="id" type="var">optimize_0plus_com</span></span>).

<div class="paragraph"> </div>

<ul class="doclist">
<li> Give a meaningful example of this optimizer's output.

<div class="paragraph"> </div>


</li>
<li> Prove that the optimizer is sound.  (This part should be <i>very</i>
     easy.)  
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab34"></a><h1 class="section">Proving Inequivalence</h1>

<div class="paragraph"> </div>

 Suppose that <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> is a command of the form <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>;;</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>
    and <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> is the command <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span>;;</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode"><span class="id" type="var">a<sub>2</sub>'</span></span>, where <span class="inlinecode"><span class="id" type="var">a<sub>2</sub>'</span></span> is
    formed by substituting <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span> for all occurrences of <span class="inlinecode"><span class="id" type="var">X</span></span> in <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>.
    For example, <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> might be:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;&nbsp;=&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;42&nbsp;+&nbsp;53;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;+&nbsp;<span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span>&nbsp;&nbsp;=&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;42&nbsp;+&nbsp;53;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;+&nbsp;(42&nbsp;+&nbsp;53))
<div class="paragraph"> </div>

</div>
    Clearly, this <i>particular</i> <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> are equivalent.  Is this
    true in general? 
<div class="paragraph"> </div>

 We will see in a moment that it is not, but it is worthwhile
    to pause, now, and see if you can find a counter-example on your
    own. 
<div class="paragraph"> </div>

 More formally, here is the function that substitutes an arithmetic
    expression <span class="inlinecode"><span class="id" type="var">u</span></span> for each occurrence of a given variable <span class="inlinecode"><span class="id" type="var">x</span></span> in
    another expression <span class="inlinecode"><span class="id" type="var">a</span></span>: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">subst_aexp</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">u</span> : <span class="id" type="var">aexp</span>) (<span class="id" type="var">a</span> : <span class="id" type="var">aexp</span>) : <span class="id" type="var">aexp</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">a</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">ANum</span> <span class="id" type="var">n</span>       ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">ANum</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">AId</span> <span class="id" type="var">x'</span>       ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">if</span> <span class="id" type="var">eqb_string</span> <span class="id" type="var">x</span> <span class="id" type="var">x'</span> <span class="id" type="keyword">then</span> <span class="id" type="var">u</span> <span class="id" type="keyword">else</span> <span class="id" type="var">AId</span> <span class="id" type="var">x'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">APlus</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMinus</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">AMult</span> (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>1</sub></span>) (<span class="id" type="var">subst_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">u</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">subst_aexp_ex</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">subst_aexp</span> <span class="id" type="var">X</span> (42 + 53) (<span class="id" type="var">Y</span> + <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;= (<span class="id" type="var">Y</span> + (42 + 53))%<span class="id" type="var">imp</span>.<br/>
<div class="togglescript" id="proofcontrol25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')"><span class="show"></span></div>
<div class="proofscript" id="proof25" onclick="toggleDisplay('proof25');toggleDisplay('proofcontrol25')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
And here is the property we are interested in, expressing the
    claim that commands <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> as described above are
    always equivalent.  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">subst_equiv_property</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">x<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> (<span class="id" type="var">x<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">x<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">x<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">subst_aexp</span> <span class="id" type="var">x<sub>1</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>).<br/>
</div>

<div class="doc">
Sadly, the property does <i>not</i> always hold &mdash; i.e., it is not the
    case that, for all <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">x<sub>2</sub></span></span>, <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>,

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">subst_aexp</span>&nbsp;<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
    To see this, suppose (for a contradiction) that for all <span class="inlinecode"><span class="id" type="var">x<sub>1</sub></span></span>, <span class="inlinecode"><span class="id" type="var">x<sub>2</sub></span></span>,
    <span class="inlinecode"><span class="id" type="var">a<sub>1</sub></span></span>, and <span class="inlinecode"><span class="id" type="var">a<sub>2</sub></span></span>, we have

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>;;&nbsp;<span class="id" type="var">x<sub>2</sub></span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">subst_aexp</span>&nbsp;<span class="id" type="var">x<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>1</sub></span>&nbsp;<span class="id" type="var">a<sub>2</sub></span>).
<div class="paragraph"> </div>

</div>
    Consider the following program:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>
<div class="paragraph"> </div>

</div>
    Note that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>1</sub></span>,
<div class="paragraph"> </div>

</div>
    where <span class="inlinecode"><span class="id" type="var">st<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">Y</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1</span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1)</span>.

<div class="paragraph"> </div>

    By assumption, we know that

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">cequiv</span>&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1)
<div class="paragraph"> </div>

</div>
    so, by the definition of <span class="inlinecode"><span class="id" type="var">cequiv</span></span>, we have

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>1</sub></span>.
<div class="paragraph"> </div>

</div>
    But we can also derive

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">empty_st</span>&nbsp;=[&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1;;&nbsp;<span class="id" type="var">Y</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;+&nbsp;1&nbsp;]⇒&nbsp;<span class="id" type="var">st<sub>2</sub></span>,
<div class="paragraph"> </div>

</div>
    where <span class="inlinecode"><span class="id" type="var">st<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" type="var">Y</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">2</span> <span class="inlinecode">;</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span> <span class="inlinecode">1)</span>.  But <span class="inlinecode"><span class="id" type="var">st<sub>1</sub></span></span> <span class="inlinecode">≠</span> <span class="inlinecode"><span class="id" type="var">st<sub>2</sub></span></span>, which is a
    contradiction, since <span class="inlinecode"><span class="id" type="var">ceval</span></span> is deterministic!  <span class="proofbox">&#9744;</span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subst_inequiv</span> :<br/>
&nbsp;&nbsp;¬<span class="id" type="var">subst_equiv_property</span>.<br/>
<div class="togglescript" id="proofcontrol26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')"><span class="show"></span></div>
<div class="proofscript" id="proof26" onclick="toggleDisplay('proof26');toggleDisplay('proofcontrol26')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">subst_equiv_property</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">Contra</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Here&nbsp;is&nbsp;the&nbsp;counterexample:&nbsp;assuming&nbsp;that&nbsp;<span class="inlinecode"><span class="id" type="var">subst_equiv_property</span></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;holds&nbsp;allows&nbsp;us&nbsp;to&nbsp;prove&nbsp;that&nbsp;these&nbsp;two&nbsp;programs&nbsp;are<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;equivalent...&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> <span class="id" type="var">c<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1)%<span class="id" type="var">imp</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> <span class="id" type="var">c<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">cequiv</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) <span class="id" type="tactic">by</span> (<span class="id" type="tactic">subst</span>; <span class="id" type="tactic">apply</span> <span class="id" type="var">Contra</span>).<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;...&nbsp;allows&nbsp;us&nbsp;to&nbsp;show&nbsp;that&nbsp;the&nbsp;command&nbsp;<span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span>&nbsp;can&nbsp;terminate<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in&nbsp;two&nbsp;different&nbsp;final&nbsp;states:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;st<sub>1</sub>&nbsp;=&nbsp;(Y&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1&nbsp;;&nbsp;X&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;st<sub>2</sub>&nbsp;=&nbsp;(Y&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;2&nbsp;;&nbsp;X&nbsp;!<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;1).&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1) <span class="id" type="keyword">as</span> <span class="id" type="var">st<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Y</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 2 ; <span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1) <span class="id" type="keyword">as</span> <span class="id" type="var">st<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">empty_st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st<sub>1</sub></span>);<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">empty_st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st<sub>2</sub></span>);<br/>
&nbsp;&nbsp;<span class="id" type="tactic">try</span> (<span class="id" type="tactic">subst</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Seq</span> <span class="id" type="keyword">with</span> (<span class="id" type="var">st'</span> := (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 1));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E_Ass</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H<sub>1</sub></span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Finally,&nbsp;we&nbsp;use&nbsp;the&nbsp;fact&nbsp;that&nbsp;evaluation&nbsp;is&nbsp;deterministic<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;to&nbsp;obtain&nbsp;a&nbsp;contradiction.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hcontra</span> : <span class="id" type="var">st<sub>1</sub></span> = <span class="id" type="var">st<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> (<span class="id" type="tactic">apply</span> (<span class="id" type="var">ceval_deterministic</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">empty_st</span>); <span class="id" type="tactic">assumption</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">Hcontra'</span> : <span class="id" type="var">st<sub>1</sub></span> <span class="id" type="var">Y</span> = <span class="id" type="var">st<sub>2</sub></span> <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">by</span> (<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hcontra</span>; <span class="id" type="tactic">reflexivity</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">subst</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">Hcontra'</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab35"></a><h4 class="section">Exercise: 4 stars, standard, optional (better_subst_equiv)</h4>
 The equivalence we had in mind above was not complete nonsense &mdash;
    it was actually almost right.  To make it correct, we just need to
    exclude the case where the variable <span class="inlinecode"><span class="id" type="var">X</span></span> occurs in the
    right-hand-side of the first assignment statement. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">var_not_used_in_aexp</span> (<span class="id" type="var">x</span> : <span class="id" type="var">string</span>) : <span class="id" type="var">aexp</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUNum</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">ANum</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUId</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">y</span>, <span class="id" type="var">x</span> ≠ <span class="id" type="var">y</span> → <span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AId</span> <span class="id" type="var">y</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUPlus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">APlus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUMinus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AMinus</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">VNUMult</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> (<span class="id" type="var">AMult</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">aeval_weakening</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span> <span class="id" type="var">st</span> <span class="id" type="var">a</span> <span class="id" type="var">ni</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">x</span> <span class="id" type="var">a</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">aeval</span> (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">ni</span> ; <span class="id" type="var">st</span>) <span class="id" type="var">a</span> = <span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Using <span class="inlinecode"><span class="id" type="var">var_not_used_in_aexp</span></span>, formalize and prove a correct version
    of <span class="inlinecode"><span class="id" type="var">subst_equiv_property</span></span>. 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab36"></a><h4 class="section">Exercise: 3 stars, standard (inequiv_exercise)</h4>
 Prove that an infinite loop is not equivalent to <span class="inlinecode"><span class="id" type="var">SKIP</span></span> 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inequiv_exercise</span>:<br/>
&nbsp;&nbsp;¬<span class="id" type="var">cequiv</span> (<span class="id" type="var">WHILE</span> <span class="id" type="var">true</span> <span class="id" type="var">DO</span> <span class="id" type="var">SKIP</span> <span class="id" type="var">END</span>) <span class="id" type="var">SKIP</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab37"></a><h1 class="section">Extended Exercise: Nondeterministic Imp</h1>

<div class="paragraph"> </div>

 As we have seen (in theorem <span class="inlinecode"><span class="id" type="var">ceval_deterministic</span></span> in the <span class="inlinecode"><span class="id" type="var">Imp</span></span>
    chapter), Imp's evaluation relation is deterministic.  However,
    <i>non</i>-determinism is an important part of the definition of many
    real programming languages. For example, in many imperative
    languages (such as C and its relatives), the order in which
    function arguments are evaluated is unspecified.  The program
    fragment

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span>&nbsp;=&nbsp;0;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">f</span>(++<span class="id" type="var">x</span>,&nbsp;<span class="id" type="var">x</span>)
<div class="paragraph"> </div>

</div>
    might call <span class="inlinecode"><span class="id" type="var">f</span></span> with arguments <span class="inlinecode">(1,</span> <span class="inlinecode">0)</span> or <span class="inlinecode">(1,</span> <span class="inlinecode">1)</span>, depending how
    the compiler chooses to order things.  This can be a little
    confusing for programmers, but it gives the compiler writer useful
    freedom.

<div class="paragraph"> </div>

    In this exercise, we will extend Imp with a simple
    nondeterministic command and study how this change affects
    program equivalence.  The new command has the syntax <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>,
    where <span class="inlinecode"><span class="id" type="var">X</span></span> is an identifier. The effect of executing <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> is
    to assign an <i>arbitrary</i> number to the variable <span class="inlinecode"><span class="id" type="var">X</span></span>,
    nondeterministically. For example, after executing the program:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span>&nbsp;<span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">Z</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">Y</span>&nbsp;*&nbsp;2
<div class="paragraph"> </div>

</div>
    the value of <span class="inlinecode"><span class="id" type="var">Y</span></span> can be any number, while the value of <span class="inlinecode"><span class="id" type="var">Z</span></span> is
    twice that of <span class="inlinecode"><span class="id" type="var">Y</span></span> (so <span class="inlinecode"><span class="id" type="var">Z</span></span> is always even). Note that we are not
    saying anything about the <i>probabilities</i> of the outcomes &mdash; just
    that there are (infinitely) many different outcomes that can
    possibly happen after executing this nondeterministic code.

<div class="paragraph"> </div>

    In a sense, a variable on which we do <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> roughly corresponds
    to an uninitialized variable in a low-level language like C.  After
    the <span class="inlinecode"><span class="id" type="var">HAVOC</span></span>, the variable holds a fixed but arbitrary number.  Most
    sources of nondeterminism in language definitions are there
    precisely because programmers don't care which choice is made (and
    so it is good to leave it open to the compiler to choose whichever
    will run faster).

<div class="paragraph"> </div>

    We call this new language <i>Himp</i> (``Imp extended with <span class="inlinecode"><span class="id" type="var">HAVOC</span></span>''). 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Himp</span>.<br/>
</div>

<div class="doc">
To formalize Himp, we first add a clause to the definition of
    commands. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">com</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">CSkip</span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CAss</span> : <span class="id" type="var">string</span> → <span class="id" type="var">aexp</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CSeq</span> : <span class="id" type="var">com</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CIf</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CWhile</span> : <span class="id" type="var">bexp</span> → <span class="id" type="var">com</span> → <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">CHavoc</span> : <span class="id" type="var">string</span> → <span class="id" type="var">com</span>. <span class="comment">(*&nbsp;&lt;---&nbsp;NEW&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "'SKIP'" :=<br/>
&nbsp;&nbsp;<span class="id" type="var">CSkip</span> : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "X '<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>' a" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CAss</span> <span class="id" type="var">X</span> <span class="id" type="var">a</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "c<sub>1</sub> ;; c<sub>2</sub>" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CSeq</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'WHILE' b 'DO' c 'END'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CWhile</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'TEST' e<sub>1</sub> 'THEN' e<sub>2</sub> 'ELSE' e<sub>3</sub> 'FI'" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CIf</span> <span class="id" type="var">e<sub>1</sub></span> <span class="id" type="var">e<sub>2</sub></span> <span class="id" type="var">e<sub>3</sub></span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>) : <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Notation</span> "'HAVOC' l" :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">CHavoc</span> <span class="id" type="var">l</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60) : <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
<a name="lab38"></a><h4 class="section">Exercise: 2 stars, standard (himp_ceval)</h4>
 Now, we must extend the operational semantics. We have provided
   a template for the <span class="inlinecode"><span class="id" type="var">ceval</span></span> relation below, specifying the big-step
   semantics. What rule(s) must be added to the definition of <span class="inlinecode"><span class="id" type="var">ceval</span></span>
   to formalize the behavior of the <span class="inlinecode"><span class="id" type="var">HAVOC</span></span> command? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Reserved Notation</span> "st '=[' c ']⇒' st'" (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 40).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Open</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">ceval</span> : <span class="id" type="var">com</span> → <span class="id" type="var">state</span> → <span class="id" type="var">state</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Skip</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">SKIP</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Ass</span>  : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">n</span> <span class="id" type="var">x</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">aeval</span> <span class="id" type="var">st</span> <span class="id" type="var">a<sub>1</sub></span> = <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">x</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span> ]⇒ (<span class="id" type="var">x</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> <span class="id" type="var">n</span> ; <span class="id" type="var">st</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">E_Seq</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>  →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c<sub>1</sub></span> ;; <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st''</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_IfFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">b</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">TEST</span> <span class="id" type="var">b</span> <span class="id" type="var">THEN</span> <span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">ELSE</span> <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">FI</span> ]⇒ <span class="id" type="var">st'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileFalse</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">b</span> <span class="id" type="var">st</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">false</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">E_WhileTrue</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> <span class="id" type="var">st''</span> <span class="id" type="var">b</span> <span class="id" type="var">c</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">beval</span> <span class="id" type="var">st</span> <span class="id" type="var">b</span> = <span class="id" type="var">true</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">c</span> ]⇒ <span class="id" type="var">st'</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st'</span> =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">st</span>  =[ <span class="id" type="var">WHILE</span> <span class="id" type="var">b</span> <span class="id" type="var">DO</span> <span class="id" type="var">c</span> <span class="id" type="var">END</span> ]⇒ <span class="id" type="var">st''</span><br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<br/>
&nbsp;&nbsp;<span class="id" type="keyword">where</span> "st =[ c ]⇒ st'" := (<span class="id" type="var">ceval</span> <span class="id" type="var">c</span> <span class="id" type="var">st</span> <span class="id" type="var">st'</span>).<br/>
<span class="id" type="var">Close</span> <span class="id" type="keyword">Scope</span> <span class="id" type="var">imp_scope</span>.<br/>
</div>

<div class="doc">
As a sanity check, the following claims should be provable for
    your definition: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">havoc_example1</span> : <span class="id" type="var">empty_st</span> =[ (<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span> ]⇒ (<span class="id" type="var">X</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 0).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">havoc_example2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">empty_st</span> =[ (<span class="id" type="var">SKIP</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Z</span>)%<span class="id" type="var">imp</span> ]⇒ (<span class="id" type="var">Z</span> !<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span> 42).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_Check_rule_for_HAVOC</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Finally, we repeat the definition of command equivalence from above: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cequiv</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> ↔ <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
</div>

<div class="doc">
Let's apply this definition to prove some nondeterministic
    programs equivalent / inequivalent. 
<div class="paragraph"> </div>

<a name="lab39"></a><h4 class="section">Exercise: 3 stars, standard (havoc_swap)</h4>
 Are the following two programs equivalent? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">pXY</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pYX</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
If you think they are equivalent, prove it. If you think they are
    not, prove that. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pXY_cequiv_pYX</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">pXY</span> <span class="id" type="var">pYX</span> ∨ ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">pXY</span> <span class="id" type="var">pYX</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab40"></a><h4 class="section">Exercise: 4 stars, standard, optional (havoc_copy)</h4>
 Are the following two programs equivalent? 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">ptwice</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">pcopy</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;; <span class="id" type="var">Y</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
If you think they are equivalent, then prove it. If you think they
    are not, then prove that.  (Hint: You may find the <span class="inlinecode"><span class="id" type="tactic">assert</span></span> tactic
    useful.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ptwice_cequiv_pcopy</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span> <span class="id" type="var">ptwice</span> <span class="id" type="var">pcopy</span> ∨ ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">ptwice</span> <span class="id" type="var">pcopy</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The definition of program equivalence we are using here has some
    subtle consequences on programs that may loop forever.  What
    <span class="inlinecode"><span class="id" type="var">cequiv</span></span> says is that the set of possible <i>terminating</i> outcomes
    of two equivalent programs is the same. However, in a language
    with nondeterminism, like Himp, some programs always terminate,
    some programs always diverge, and some programs can
    nondeterministically terminate in some runs and diverge in
    others. The final part of the following exercise illustrates this
    phenomenon.

<div class="paragraph"> </div>

<a name="lab41"></a><h4 class="section">Exercise: 4 stars, advanced (p1_p2_term)</h4>
 Consider the following commands: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>1</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ¬(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">Y</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">X</span> + 1<br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>2</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ¬(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">SKIP</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/>
</div>

<div class="doc">
Intuitively, <span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> have the same termination behavior:
    either they loop forever, or they terminate in the same state they
    started in.  We can capture the termination behavior of <span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> and
    <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> individually with these lemmas: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">p1_may_diverge</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span>, <span class="id" type="var">st</span> <span class="id" type="var">X</span> ≠ 0 →<br/>
&nbsp;&nbsp;¬<span class="id" type="var">st</span> =[ <span class="id" type="var">p<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">p2_may_diverge</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">st</span> <span class="id" type="var">st'</span>, <span class="id" type="var">st</span> <span class="id" type="var">X</span> ≠ 0 →<br/>
&nbsp;&nbsp;¬<span class="id" type="var">st</span> =[ <span class="id" type="var">p<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab42"></a><h4 class="section">Exercise: 4 stars, advanced (p1_p2_equiv)</h4>
 Use these two lemmas to prove that <span class="inlinecode"><span class="id" type="var">p<sub>1</sub></span></span> and <span class="inlinecode"><span class="id" type="var">p<sub>2</sub></span></span> are actually
    equivalent. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p1_p2_equiv</span> : <span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>1</sub></span> <span class="id" type="var">p<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab43"></a><h4 class="section">Exercise: 4 stars, advanced (p3_p4_inequiv)</h4>
 Prove that the following programs are <i>not</i> equivalent.  (Hint:
    What should the value of <span class="inlinecode"><span class="id" type="var">Z</span></span> be when <span class="inlinecode"><span class="id" type="var">p<sub>3</sub></span></span> terminates?  What about
    <span class="inlinecode"><span class="id" type="var">p<sub>4</sub></span></span>?) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>3</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1;;<br/>
&nbsp;&nbsp;<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 0) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span>;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">Z</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>4</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 0;;<br/>
&nbsp;&nbsp;<span class="id" type="var">Z</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p3_p4_inequiv</span> : ¬<span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>3</sub></span> <span class="id" type="var">p<sub>4</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab44"></a><h4 class="section">Exercise: 5 stars, advanced, optional (p5_p6_equiv)</h4>
 Prove that the following commands are equivalent.  (Hint: As
    mentioned above, our definition of <span class="inlinecode"><span class="id" type="var">cequiv</span></span> for Himp only takes
    into account the sets of possible terminating configurations: two
    programs are equivalent if and only if the set of possible terminating
    states is the same for both programs when given a same starting state
    <span class="inlinecode"><span class="id" type="var">st</span></span>.  If <span class="inlinecode"><span class="id" type="var">p<sub>5</sub></span></span> terminates, what should the final state be? Conversely,
    is it always possible to make <span class="inlinecode"><span class="id" type="var">p<sub>5</sub></span></span> terminate?) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>5</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">WHILE</span> ~(<span class="id" type="var">X</span> = 1) <span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">HAVOC</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;<span class="id" type="var">END</span>)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">p<sub>6</sub></span> : <span class="id" type="var">com</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">X</span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> 1)%<span class="id" type="var">imp</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">p5_p6_equiv</span> : <span class="id" type="var">cequiv</span> <span class="id" type="var">p<sub>5</sub></span> <span class="id" type="var">p<sub>6</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Himp</span>.<br/>
</div>

<div class="doc">
<a name="lab45"></a><h1 class="section">Additional Exercises</h1>

<div class="paragraph"> </div>

<a name="lab46"></a><h4 class="section">Exercise: 4 stars, standard, optional (for_while_equiv)</h4>
 This exercise extends the optional <span class="inlinecode"><span class="id" type="var">add_for_loop</span></span> exercise from
    the <a href="https://www.cis.upenn.edu/~bcpierce/sf/lf-current/Imp.html"><span class="inlineref">Imp</span></a> chapter, where you were asked to extend the language
    of commands with C-style <span class="inlinecode"><span class="id" type="keyword">for</span></span> loops.  Prove that the command:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">for</span>&nbsp;(<span class="id" type="var">c<sub>1</sub></span>&nbsp;;&nbsp;<span class="id" type="var">b</span>&nbsp;;&nbsp;<span class="id" type="var">c<sub>2</sub></span>)&nbsp;{<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>3</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}
<div class="paragraph"> </div>

</div>
    is equivalent to:

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">WHILE</span>&nbsp;<span class="id" type="var">b</span>&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>3</sub></span>&nbsp;;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">c<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab47"></a><h4 class="section">Exercise: 3 stars, standard, optional (swap_noninterfering_assignments)</h4>
 (Hint: You'll need <span class="inlinecode"><span class="id" type="var">functional_extensionality</span></span> for this one.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">swap_noninterfering_assignments</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">l<sub>1</sub></span> ≠ <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">a<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">var_not_used_in_aexp</span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">a<sub>1</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">cequiv</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">l<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>;; <span class="id" type="var">l<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">l<sub>2</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>2</sub></span>;; <span class="id" type="var">l<sub>1</sub></span> <span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span> <span class="id" type="var">a<sub>1</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab48"></a><h4 class="section">Exercise: 4 stars, advanced, optional (capprox)</h4>
 In this exercise we define an asymmetric variant of program
    equivalence we call <i>program approximation</i>. We say that a
    program <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> <i>approximates</i> a program <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> when, for each of
    the initial states for which <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> terminates, <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> also terminates
    and produces the same final state. Formally, program approximation
    is defined as follows: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">capprox</span> (<span class="id" type="var">c<sub>1</sub></span> <span class="id" type="var">c<sub>2</sub></span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span> := <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">st</span> <span class="id" type="var">st'</span> : <span class="id" type="var">state</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>1</sub></span> ]⇒ <span class="id" type="var">st'</span> → <span class="id" type="var">st</span> =[ <span class="id" type="var">c<sub>2</sub></span> ]⇒ <span class="id" type="var">st'</span>.<br/>
</div>

<div class="doc">
For example, the program

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;=&nbsp;<span class="id" type="var">WHILE</span>&nbsp;~(<span class="id" type="var">X</span>&nbsp;=&nbsp;1)&nbsp;<span class="id" type="var">DO</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">X</span>&nbsp;<span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span>&nbsp;<span class="id" type="var">X</span>&nbsp;-&nbsp;1<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">END</span>
<div class="paragraph"> </div>

</div>
    approximates <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span> <span class="inlinecode">1</span>, but <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> does not approximate <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span>
    since <span class="inlinecode"><span class="id" type="var">c<sub>1</sub></span></span> does not terminate when <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> but <span class="inlinecode"><span class="id" type="var">c<sub>2</sub></span></span> does.  If two
    programs approximate each other in both directions, then they are
    equivalent. 
<div class="paragraph"> </div>

 Find two programs <span class="inlinecode"><span class="id" type="var">c<sub>3</sub></span></span> and <span class="inlinecode"><span class="id" type="var">c<sub>4</sub></span></span> such that neither approximates
    the other. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">c<sub>3</sub></span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">c<sub>4</sub></span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">c3_c4_different</span> : ¬<span class="id" type="var">capprox</span> <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">c<sub>4</sub></span> ∧ ¬<span class="id" type="var">capprox</span> <span class="id" type="var">c<sub>4</sub></span> <span class="id" type="var">c<sub>3</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Find a program <span class="inlinecode"><span class="id" type="var">cmin</span></span> that approximates every other program. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">cmin</span> : <span class="id" type="var">com</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">cmin_minimal</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span>, <span class="id" type="var">capprox</span> <span class="id" type="var">cmin</span> <span class="id" type="var">c</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
Finally, find a non-trivial property which is preserved by
    program approximation (when going from left to right). 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">zprop</span> (<span class="id" type="var">c</span> : <span class="id" type="var">com</span>) : <span class="id" type="keyword">Prop</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">zprop_preserving</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">c</span> <span class="id" type="var">c'</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">zprop</span> <span class="id" type="var">c</span> → <span class="id" type="var">capprox</span> <span class="id" type="var">c</span> <span class="id" type="var">c'</span> → <span class="id" type="var">zprop</span> <span class="id" type="var">c'</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Thu&nbsp;Feb&nbsp;7&nbsp;20:09:23&nbsp;EST&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>